Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    from(X)  → cons(X,n__from(n__s(X)))
2:    2ndspos(0,Z)  → rnil
3:    2ndspos(s(N),cons(X,Z))  → 2ndspos(s(N),cons2(X,activate(Z)))
4:    2ndspos(s(N),cons2(X,cons(Y,Z)))  → rcons(posrecip(Y),2ndsneg(N,activate(Z)))
5:    2ndsneg(0,Z)  → rnil
6:    2ndsneg(s(N),cons(X,Z))  → 2ndsneg(s(N),cons2(X,activate(Z)))
7:    2ndsneg(s(N),cons2(X,cons(Y,Z)))  → rcons(negrecip(Y),2ndspos(N,activate(Z)))
8:    pi(X)  → 2ndspos(X,from(0))
9:    plus(0,Y)  → Y
10:    plus(s(X),Y)  → s(plus(X,Y))
11:    times(0,Y)  → 0
12:    times(s(X),Y)  → plus(Y,times(X,Y))
13:    square(X)  → times(X,X)
14:    from(X)  → n__from(X)
15:    s(X)  → n__s(X)
16:    activate(n__from(X))  → from(activate(X))
17:    activate(n__s(X))  → s(activate(X))
18:    activate(X)  → X
There are 19 dependency pairs:
19:    2ndspos#(s(N),cons(X,Z))  → 2ndspos#(s(N),cons2(X,activate(Z)))
20:    2ndspos#(s(N),cons(X,Z))  → ACTIVATE(Z)
21:    2ndspos#(s(N),cons2(X,cons(Y,Z)))  → 2ndsneg#(N,activate(Z))
22:    2ndspos#(s(N),cons2(X,cons(Y,Z)))  → ACTIVATE(Z)
23:    2ndsneg#(s(N),cons(X,Z))  → 2ndsneg#(s(N),cons2(X,activate(Z)))
24:    2ndsneg#(s(N),cons(X,Z))  → ACTIVATE(Z)
25:    2ndsneg#(s(N),cons2(X,cons(Y,Z)))  → 2ndspos#(N,activate(Z))
26:    2ndsneg#(s(N),cons2(X,cons(Y,Z)))  → ACTIVATE(Z)
27:    PI(X)  → 2ndspos#(X,from(0))
28:    PI(X)  → FROM(0)
29:    PLUS(s(X),Y)  → S(plus(X,Y))
30:    PLUS(s(X),Y)  → PLUS(X,Y)
31:    TIMES(s(X),Y)  → PLUS(Y,times(X,Y))
32:    TIMES(s(X),Y)  → TIMES(X,Y)
33:    SQUARE(X)  → TIMES(X,X)
34:    ACTIVATE(n__from(X))  → FROM(activate(X))
35:    ACTIVATE(n__from(X))  → ACTIVATE(X)
36:    ACTIVATE(n__s(X))  → S(activate(X))
37:    ACTIVATE(n__s(X))  → ACTIVATE(X)
The approximated dependency graph contains 4 SCCs: {35,37}, {19,21,23,25}, {30} and {32}. Hence the TRS is terminating.
Tyrolean Termination Tool  (2.40 seconds)   ---  May 3, 2006